The general form a type checking rule is:
\[ \frac{\vdots}{O,M,C \vdash e : T} \]The rule should be read: In the type environment for objects \(O\), methods \(M\), and containing class \(C\), the expression \(e\) has type \(T\). The dots above the horizontal bar stand for other statements about the types of sub-expressions of \(e\). These other statements are hypotheses of the rule; if the hypotheses are satisfied, then the statement below the bar is true. In the conclusion, the "turnstile" ("\(\vdash\)") separates context (\(O,M,C\)) from statement (\(e : T\)).
The rule for object identifiers is simply that if the environment assigns an identifier \(Id\) type \(T\), then \(Id\) has type \(T\).
\[ \frac{O(Id) = T}{O,M,C \vdash Id : T}\mbox{[Var]} \]The rule for assignment to a variable is more complex:
\[ \frac{ \begin{array}{l} O(Id) = T \\ O,M,C \vdash e_1 : T' \\ T' \le T \\ \end{array} }{O,M,C \vdash Id \leftarrow e_1 : T'}\mbox{[ASSIGN]} \]Note that this type rule--as well as others--use the conformance relation \(\leq\) (see Section 3.2). The rule says that the assigned expression \(e_1\) must have a type \(T'\) that conforms to the type \(T\) of the identifier \(Id\) in the type environment. The type of the whole expression is \(T'\). The type rules for constants are all easy:
\[ \frac{}{O,M,C \vdash true:Bool}\mbox{[True]} \] \[ \frac{}{O,M,C \vdash false:Bool}\mbox{[False]} \] \[ \frac{i\ {\rm is\ an\ integer\ constant}}{O,M,C \vdash i:Int}\mbox{[Int]} \] \[ \frac{s\ {\rm is\ an\ string\ constant}}{O,M,C \vdash s:String}\mbox{[String]} \]There are two cases for new, one for new SELF_TYPE and one for any other form:
\[ \frac{ T' = \left\{ \begin{array}{rl} {\rm SELF\_TYPE_C} & {\rm if}\ T = {\rm SELF\_TYPE} \\ T & {\rm otherwise} \end{array} \right. }{O,M,C\vdash new\ T:T'}\mbox{[New]} \]Dispatch expressions are the most complex to type check.
\[ \frac{ \begin{array}{l} O,M,C \vdash e_0:T_0 \\ O,M,C \vdash e_1:T_1 \\ \vdots \\ O,M,C \vdash e_n:T_n \\ T'_0 = \left\{ \begin{array}{rl} C & {\rm if}\ T_0 = {\rm SELF\_TYPE_C} \\ T_0 & {\rm otherwise} \end{array} \right. \\ M(T'_0,f)=(T'_1,\ldots,T'_n,T'_{n+1}) \\ T_i \le T'_i\quad 1 \le i \le n \\ T_{n+1} = \left\{ \begin{array}{rl} T_0 & {\rm if}\ T'_{n+1}={\rm SELF\_TYPE} \\ T'_{n+1} & {\rm otherwise} \end{array} \right. \end{array} }{O,M,C \vdash e_0.f(e_1,\ldots,e_n):T_{n+1}}\mbox{[Dispatch]} \] \[ \frac{ \begin{array}{l} O,M,C \vdash e_0:T_0 \\ O,M,C \vdash e_1:T_1 \\ \vdots \\ O,M,C \vdash e_n:T_n \\ T_0 \le T \\ M(T,f)=(T'_1,\ldots,T'_n,T'_{n+1}) \\ T_i \le T'_i\quad 1 \le i \le n \\ T_{n+1} = \left\{ \begin{array}{rl} T_0 & {\rm if}\ T'_{n+1}={\rm SELF\_TYPE} \\ T'_{n+1} & {\rm otherwise} \end{array} \right. \end{array} }{O,M,C \vdash e_0@T.f(e_1,\ldots,e_n):T_{n+1}}\mbox{[Static Dispatch]} \]To type check a dispatch, each of the subexpressions must first be type checked. The type \(T_0\) of \(e_0\) determines which declaration of the method \(f\) is used. The argument types of the dispatch must conform to the declared argument types. Note that the type of the result of the dispatch is either the declared return type or \(T_0\) in the case that the declared return type is \(\tt SELF\_TYPE\). The only difference in type checking a static dispatch is that the class \(T\) of the method \(f\) is given in the dispatch, and the type \(T_0\) must conform to \(T\).
The type checking rules for \(\rm if\) and \(\rm \{ \HY \}\) expressions are straightforward. See Section 7.5 for the definition of the \(\sqcup\) operation.
\[ \frac{\begin{array}{l} O,M,C \vdash e_1:Bool \\ O,M,C \vdash e_2:T_2 \\ O,M,C \vdash e_3:T_3 \end{array}} {O,M,C \vdash {\rm if}\ e_1\ {\rm then}\ e_2\ {\rm else}\ e_3\ {\rm fi}:T_2\sqcup T_3}\mbox{[If]} \] \[ \frac{\begin{array}{l} O,M,C \vdash e_1:T_1 \\ O,M,C \vdash e_2:T_2 \\ \vdots \\ O,M,C \vdash e_n:T_n \end{array}} {O,M,C \vdash \{\ e_1;e_2;\ldots e_n;\ \}:T_n}\mbox{[Sequence]} \]The \(\rm let\) rule has some interesting aspects.
\[ \frac{\begin{array}{l} T'_0 = \left\{ \begin{array}{rl} {\tt SELF\_TYPE_C} & {\rm if}\ T_0 = {\tt SELF\_TYPE} \\ T_0 & {\rm otherwise} \end{array} \right. \\ O,M,C \vdash e_1:T_1 \\ T_1 \le T'_0 \\ O[T'_0/x],M,C \vdash e_2:T_2 \end{array}} {O,M,C \vdash {\rm let}\ x: T_0 \leftarrow e_1\ in\ e_2:T_2}\mbox{[Let-Init]} \]First, the initialization \(e_1\) is type checked in an environment without a new definition for \(x\). Thus, the variable \(x\) cannot be used in \(e_1\) unless it already has a definition in an outer scope. Second, the body \(e_2\) is type checked in the environment \(O\) extended with the typing \(x:T_0'\). Third, note that the type of \(x\) may be \(\rm SELF\_TYPE\).
\[ \frac{\begin{array}{l} T'_0 = \left\{ \begin{array}{rl} {\tt SELF\_TYPE_C} & {\rm if}\ T_0 = {\tt SELF\_TYPE} \\ T_0 & {\rm otherwise} \end{array} \right. \\ O[T'_0/x],M,C \vdash e_1:T_1 \end{array}} {O,M,C \vdash {\rm let}\ x:T_0\ {\rm in}\ e_1:T_1}\mbox{[Let-No-Init]} \]The rule for \(\rm let\) with no initialization simply omits the conformance requirement. We give type rules only for a \(\rm let\) with a single variable. Typing a multiple \(\rm let\)
\[ \rm let\ x_1 : T_1\ [\leftarrow e_1],\ x_2: T_2\ [\leftarrow e_2], \ldots,\ x_n :T_n\ [\leftarrow e_n]\ in\ e \]is defined to be the same as typing
\[ \rm let\ x_1 : T_1\ [\leftarrow e_1]\ in\ (let\ x_2 :T_2\ [\leftarrow e_2],\ldots,\ x_n : T_n\ [\leftarrow e_n]\ in\ e\ )\ \] \[ \frac{\begin{array}{l} O,M,C \vdash e_0:T_0 \\ O[T_1/x_1],M,C \vdash e_1:T'_1 \\ \vdots \\ O[T_n/x_n],M,C \vdash e_n:T'_n \end{array}} {O,M,C \vdash {\rm case}\ e_0\ {\rm of}\ x_1:T_1 \Rightarrow e_1;,\ldots x_n:T_n \Rightarrow e_n;\ {\rm esac}:\sqcup_{1 \le i \le n} T'_i}\mbox{[Case]} \]Each branch of a \(\rm case\) is type checked in an environment where variable \(x_i\) has type \(T_i\). The type of the entire \(\rm case\) is the join of the types of its branches. The variables declared on each branch of a \(\rm case\) must all have distinct types.
\[ \frac{\begin{array}{l} O,M,C \vdash e_1:Bool \\ O,M,C \vdash e_2:T_2 \end{array}} {O,M,C \vdash {\rm while}\ e_1\ {\rm loop}\ e_2\ {\rm pool}:Object}\mbox{[Loop]} \]The predicate of a loop must have type \(Bool\); the type of the entire loop is always \(Object\). An \(\rm isvoid\) test has type \(Bool\):
\[ \frac{ O,M,C \vdash e_1:T_1 } {O,M,C \vdash {\rm isvoid}\ e_1:Bool}\mbox{[Isvoid]} \]With the exception of the rule for equality, the type checking rules for the primitive logical and arithmetic operations are easy.
\[ \frac{ O,M,C \vdash e_1:Bool } {O,M,C \vdash \lnot e_1:Bool}\mbox{[Not]} \] \[ \frac{ O,M,C \vdash e_1:Int } {O,M,C \vdash \sim e_1:Int}\mbox{[Neg]} \] \[ \frac{\begin{array}{l} O,M,C \vdash e_1:Int \\ O,M,C \vdash e_2:Int \\ {\rm op} \in \{*,+,-,/\} \end{array}} {O,M,C \vdash e_1\ op\ e_2:Int}\mbox{[Arith]} \]The wrinkle in the rule for equality is that any types may be freely compared except \(\rm Int\), \(\rm String\) and \(\rm Bool\), which may only be compared with objects of the same type. The cases for \(\rm <\) and \(\rm <=\) are similar to the rule for equality.
\[ \frac{\begin{array}{l} O,M,C \vdash e_1 : T_1 \\ O,M,C \vdash e_2 : T_2 \\ T_1 \in \{Int,String,Bool\} \lor T_2 \in \{Int,String,Bool\} \Rightarrow T_1 = T_2 \end{array}} {O,M,C \vdash e_1 = e_2 : Bool}\mbox{[Equal]} \]The final cases are type checking rules for attributes and methods. For a class \(C\), let the object environment \(O_C\) give the types of all attributes of \(C\) (including any inherited attributes). More formally, if \(x\) is an attribute (inherited or not) of \(C\), and the declaration of \(x\) is \(x:T\), then
\[ O_C(x) = \left\{ \begin{array}{rl} {\rm SELF\_TYPE_C} & {\rm if}\ T = {\rm SELF\_TYPE} \\ T & otherwise \end{array} \right. \]The method environment \(M\) is global to the entire program and defines for every class \(C\) the signatures of all of the methods of \(C\) (including any inherited methods).
The two rules for type checking attribute defininitions are similar the rules for \(\rm let\). The essential difference is that attributes are visible within their initialization expressions. Note that \(\rm self\) is bound in the initialization.
\[ \frac{\begin{array}{l} O_C(x) = T_0 \\ O_C [{\rm SELF\_TYPE}_C/self],M,C \vdash e_1 : T_1 \\ T_1 \le T_0 \end{array}} {O_C,M,C \vdash x : T_0 \leftarrow e_1; }\mbox{[Attr-Init]} \] \[ \frac{ O_C(x) = T } {O_C,M,C \vdash x : T;}\mbox{[Attr-No-Init]} \]The rule for typing methods checks the body of the method in an environment where \(O_C\) is extended with bindings for the formal parameters and \(\rm self\). The type of the method body must conform to the declared return type.
\[ \frac{\begin{array}{l} M(C,f) = (T_1,\ldots,T_n,T_0) \\ O_C[{\rm SELF\_TYPE}_C/self][T_1/x_1]\ldots[T_n/x_n],M,C \vdash e : T'_0 \\ T'_0 \le \left\{ \begin{array}{rl} {\rm SELF\_TYPE}_C & {\rm if}\ T_0 = {\rm SELF\_TYPE} \\ T_0 & otherwise \end{array} \right. \end{array}} {O_C,M,C \vdash f(x_1 : T_1,\ldots,x_n : T_n):T_0 \{\ e\ \};}\mbox{[Method]} \]There are a number of semantic checks applied to Cool programs that are not captured by formal typing rules. For example, a Cool program cannot contain an inheritance cycle. Similarly, a Cool program cannot contain a class that inherits from \(\rm String\). These rules are scattered through the \(\it Cool\ Reference\ Manual\).
The order in which these other checks are performed is \(\it not\ specified\). If a Cool program contains both an inheritance cycle and also a class that inherits from \(\rm String\), the Cool compiler may report whichever error it prefers.